代數 (圈)
圈$ \bf Cとその自己函手 (endofunctor)$ F:{\bf C}\to{\bf C}の F-代數とは、對象$ A\in|{\bf C}|と射$ \alpha:F(A)\to Aの組$ (A,\alpha)を言ふ 對象$ Aを F-代數$ (A,\alpha)の carrier と呼ぶ
F-代數$ (A^*,\alpha)と$ (B,\beta)が在る時、可換圖式$ \alpha;f=F(f);\betaを滿たす圈$ \bf Cの射$ f:A^*\to Bを、F-代數の準同型 (homomorphism) と呼ぶ code:tex
\begin{array}{c}
F(A^*) & \xrightarrow{\alpha} & A^* \\
_{F(f)}\darr & & \darr_{f} \\
F(B) & \xrightarrow{\beta} & B
\end{array}
F-代數の圈$ {\bf Alg}(F)とは、F-代數を對象とし準同型を射とする圈である F-代數の圈から圈$ \bf Cへの忘卻函手 (forgetfull functor) が在り、F-代數$ (A^*,\alpha)を對象$ A^*に、準同型$ f:(A^*,\alpha)\to(B,\beta)を射$ f:A^*\to Bに對應させる $ A^*を$ a_0\in A^*と$ {\rm cons}:A\times A^*\to A^*で構成 (construct) できるとすると
$ A^*からの射$ f:A^*\to Bを歸納的に$ f(a_0)=b_0、$ !\exist g_{:A\times B\to B}(f\circ {\rm cons}(x,a)=g(x,f(a)))と定義できる
歸納法原理$ P(a_0)\land\forall a_{\in A^*}(P(a)\to\forall x_{\in A}P({\rm cons}(x,a))\to\forall a_{\in A^*}P(a)
$ a_0に關する附値と$ \rm consに關する附値の等式から、全體の附値が定まる
代數は生成元から演算 (constructor) で歸納的に作り出せる
多くの代數的構造は臺集合と演算に加へて律 (等式的公理 (等式論理)) も持つ F-始代數 (initial F-algebra) 自己函手$ Fの不動點$ \mu F\in|{\bf C}|,$ \mu F\simeq F(\mu F)を取れば組$ (\mu F,F(\mu F)\to F)は F-始代數 任意の F-代數$ (X,\varphi)に對して、ただ一つ存在する射$ \mu F\to Xを catamorphism と呼び$ {\rm cata}\varphiと書く。fold() 函數に當たる
圈$ \bf Cとその自己函手 (endofunctor)$ F:{\bf C}\to{\bf C}の F-餘代數とは、對象$ A\in|{\bf C}|と射$ \alpha:A\to F(A)の組$ (A,\alpha)を言ふ 對象$ Aを F-餘代數$ (A,\alpha)の carrier と呼ぶ F-餘代數$ (B,\beta)と$ (A^\infty,\alpha)が在る時、可換圖式$ \beta;F(f)=f;\alphaを滿たす圈$ \bf Cの射$ f:B\to A^\inftyを、F-餘代數の準同型 (morphism) と呼ぶ code:tex
\begin{array}{c}
B & \xrightarrow{\beta} & F(B) \\
_{f}\darr & & \darr_{F(f)} \\
A^\infty & \xrightarrow{\alpha} & F(A^\infty)
\end{array}
F-餘代數の圈から圈$ \bf Cへの忘卻函手 (forgetfull functor) が在り、F-餘代數$ (A^\infty,\alpha)を對象$ A^\inftyに、準同型$ f:(B,\beta)\to(A^\infty,\alpha)を射$ f:B\to A^\inftyに對應させる $ A^\inftyを$ {\rm dest}:A^\infty\to A\times A^\inftyで分解 (destruct) できるとすると
分解は、不明な情報源から情報を取り出す事に當たる
$ A^\inftyへの射$ f:B\to A^\inftyを$ !\exist h_{:B\to A},t_{:B\to B}({\rm dest}\circ f(b)=\lang h(b),f\circ t(b)\rang)と餘歸納的に定義できる
餘歸納法原理 (principle of coinduction)$ \forall a((pRq\land p\xrightarrow{a}p')\to\exist q'(p'Rq'\land q\xrightarrow{a}q'))且つ$ \forall b((qR^{-1}p\land q\xrightarrow{b}q')\to\exist p'(q'R^{-1}p'\land p\xrightarrow{b}p'))ならば$ p=q?
?
$ ({\rm dest}(P(a))=\lang a_P,x\rang)\to \exist a_Q({\rm dest}(Q(a))=\lang a_Q,y\rang)且つ
$ \to p_{:A^\infty\to A\times A^\infty}=q_{:A^\infty\to A\times A^\infty}.
table:ビット列計算と餘歸納原理
代數 餘代數
bottom up top down
F-終餘代數 (terminal F-coalgebra) 自己函手$ Fの不動點$ \mu F\in|{\bf C}|,$ \mu F\simeq F(\mu F)を取れば組$ (\mu F,F\to F(\mu F))は F-終餘代數 任意の F-餘代數$ (X,\psi)に對して、ただ一つ存在する射$ X\to\mu Fを anamorphism と呼び$ {\rm ana}\psiと書く。unfold() 函數に當たる F-餘代數$ (A,\psi)の anamorphism$ {\rm ana}\psiと F-代數$ (B,\varphi)の catamorphism$ {\rm cata}\varphiとの合成$ {\rm ana}\psi;{\rm cata}\varphiを hylomorphism と呼び$ {\rm hylo}(\varphi,\psi)と書く。再歸函數に當たる 可換圖式$ {\rm hylo}(\varphi,\psi):A\to B code:tex
\begin{array}{c}
A & \xrightarrow{\psi} & F(A) \\
_{{\rm ana}\psi}\darr & & \darr_{F({\rm ana}\psi)} \\
\mu F & \xleftrightarrow{\simeq} & F(\mu F) \\
_{{\rm cata}\varphi}\darr & & \darr_{F({\rm cata}\varphi)} \\
B & \xleftarrow{\varphi} & F(B)
\end{array}
雙代數